$X$$\mid$$a$.$P$($a$)($e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case $X$($e$) of inl($a$) =$>$ if $P$($a$) then inl $a$  else inr $\cdot$  fi  $\mid$ inr($b$) =$>$ inr $b$